/-
Copyright (c) 2025 Christian Merten. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Merten
-/
module

public import Mathlib.RingTheory.Extension.Presentation.Basic

/-!
# Presentations on subrings

In this file we establish the API for realising a presentation over a
subring of `R`. We define a property `HasCoeffs R₀` for a presentation `P` to mean
the (sub)ring `R₀` contains the coefficients of the relations of `P`.
subring `R₀` of `R` that contains the coefficients of the relations
In this case there exists a model of `S` over `R₀`, i.e., there exists an `R₀`-algebra `S₀`
such that `S` is isomorphic to `R ⊗[R₀] S₀`.

If the presentation is finite, `R₀` may be chosen as a Noetherian ring. In this case,
this API can be used to remove Noetherian hypothesis in certain cases.

-/

@[expose] public section

open TensorProduct

variable {R S ι σ : Type*} [CommRing R] [CommRing S] [Algebra R S]

variable {P : Algebra.Presentation R S ι σ}

namespace Algebra.Presentation

variable (P) in
/-- The coefficients of a presentation are the coefficients of the relations. -/
def coeffs : Set R := ⋃ (i : σ), (P.relation i).coeffs

lemma coeffs_relation_subset_coeffs (x : σ) :
    ((P.relation x).coeffs : Set R) ⊆ P.coeffs :=
  Set.subset_iUnion_of_subset x (by simp)

lemma finite_coeffs [Finite σ] : P.coeffs.Finite :=
  Set.finite_iUnion fun _ ↦ Finset.finite_toSet _

variable (P) in
/-- The core of a presentation is the subalgebra generated by the coefficients of the relations. -/
def core : Subalgebra ℤ R := Algebra.adjoin _ P.coeffs

variable (P) in
lemma coeffs_subset_core : P.coeffs ⊆ P.core := Algebra.subset_adjoin

lemma coeffs_relation_subset_core (x : σ) :
    ((P.relation x).coeffs : Set R) ⊆ P.core :=
  subset_trans (P.coeffs_relation_subset_coeffs x) P.coeffs_subset_core

variable (P) in
/-- The core coerced to a type for performance reasons. -/
def Core : Type _ := P.core

instance : CommRing P.Core := fast_instance% (inferInstanceAs <| CommRing P.core)
instance : Algebra P.Core R := fast_instance% (inferInstanceAs <| Algebra P.core R)
instance : FaithfulSMul P.Core R := inferInstanceAs <| FaithfulSMul P.core R
instance : Algebra P.Core S := fast_instance% (inferInstanceAs <| Algebra P.core S)
instance : IsScalarTower P.Core R S := inferInstanceAs <| IsScalarTower P.core R S

instance [Finite σ] : FiniteType ℤ P.Core := .adjoin_of_finite P.finite_coeffs

variable (P) in
/--
A ring `R₀` has the coefficients of the presentation `P` if the coefficients of the relations of `P`
lie in the image of `R₀` in `R`.
The smallest subring of `R` satisfying this is given by `Algebra.Presentation.Core P`.
-/
class HasCoeffs (R₀ : Type*) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S]
    [IsScalarTower R₀ R S] where
  coeffs_subset_range : P.coeffs ⊆ Set.range (algebraMap R₀ R)

instance : P.HasCoeffs P.Core where
  coeffs_subset_range := by
    refine subset_trans P.coeffs_subset_core ?_
    simp [Core, Subalgebra.algebraMap_eq]

variable (R₀ : Type*) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S]
  [P.HasCoeffs R₀]

lemma coeffs_subset_range : (P.coeffs : Set R) ⊆ Set.range (algebraMap R₀ R) :=
  HasCoeffs.coeffs_subset_range

lemma HasCoeffs.of_isScalarTower {R₁ : Type*} [CommRing R₁] [Algebra R₀ R₁] [Algebra R₁ R]
    [IsScalarTower R₀ R₁ R] [Algebra R₁ S] [IsScalarTower R₁ R S] :
    P.HasCoeffs R₁ := by
  refine ⟨subset_trans (P.coeffs_subset_range R₀) ?_⟩
  simp [IsScalarTower.algebraMap_eq R₀ R₁ R, RingHom.coe_comp, Set.range_comp]

instance (s : Set R) : P.HasCoeffs (Algebra.adjoin R₀ s) := HasCoeffs.of_isScalarTower R₀

lemma HasCoeffs.coeffs_relation_mem_range (x : σ) :
    ↑(P.relation x).coeffs ⊆ Set.range (algebraMap R₀ R) :=
  subset_trans (P.coeffs_relation_subset_coeffs x) HasCoeffs.coeffs_subset_range

lemma HasCoeffs.relation_mem_range_map (x : σ) :
    P.relation x ∈ Set.range (MvPolynomial.map (algebraMap R₀ R)) := by
  rw [MvPolynomial.mem_range_map_iff_coeffs_subset]
  exact HasCoeffs.coeffs_relation_mem_range R₀ x

/-- The `r`-th relation of `P` as a polynomial in `R₀`. This is the (arbitrary) choice of a
pre-image under the map `R₀[X] → R[X]`. -/
noncomputable def relationOfHasCoeffs (r : σ) : MvPolynomial ι R₀ :=
  (HasCoeffs.relation_mem_range_map (P := P) R₀ r).choose

lemma map_relationOfHasCoeffs (r : σ) :
    MvPolynomial.map (algebraMap R₀ R) (P.relationOfHasCoeffs R₀ r) = P.relation r :=
  (HasCoeffs.relation_mem_range_map R₀ r).choose_spec

@[simp]
lemma aeval_val_relationOfHasCoeffs (r : σ) :
    MvPolynomial.aeval P.val (P.relationOfHasCoeffs R₀ r) = 0 := by
  rw [← MvPolynomial.aeval_map_algebraMap R, map_relationOfHasCoeffs, aeval_val_relation]

@[simp]
lemma algebraTensorAlgEquiv_symm_relation (r : σ) :
    (MvPolynomial.algebraTensorAlgEquiv R₀ R).symm (P.relation r) =
      1 ⊗ₜ P.relationOfHasCoeffs R₀ r := by
  rw [← map_relationOfHasCoeffs R₀, MvPolynomial.algebraTensorAlgEquiv_symm_map]

/-- The model of `S` over a `R₀` that contains the coefficients of `P` is `R₀[X]` quotiented by the
same relations. -/
abbrev ModelOfHasCoeffs : Type _ :=
  MvPolynomial ι R₀ ⧸ (Ideal.span <| Set.range (P.relationOfHasCoeffs R₀))

instance [Finite ι] [Finite σ] : Algebra.FinitePresentation R₀ (P.ModelOfHasCoeffs R₀) := by
  classical
  cases nonempty_fintype σ
  exact .quotient ⟨Finset.image (P.relationOfHasCoeffs R₀) .univ, by simp⟩

variable (P) in
/-- (Implementation detail): The underlying `AlgHom` of `tensorModelOfHasCoeffsEquiv`. -/
noncomputable def tensorModelOfHasCoeffsHom : R ⊗[R₀] P.ModelOfHasCoeffs R₀ →ₐ[R] S :=
  Algebra.TensorProduct.lift (Algebra.ofId R S)
    (Ideal.Quotient.liftₐ _ (MvPolynomial.aeval P.val) <| by
      simp_rw [← RingHom.mem_ker, ← SetLike.le_def, Ideal.span_le]
      rintro a ⟨i, rfl⟩
      simp)
    fun _ _ ↦ Commute.all _ _

@[simp]
lemma tensorModelOfHasCoeffsHom_tmul (x : R) (y : MvPolynomial ι R₀) :
    P.tensorModelOfHasCoeffsHom R₀ (x ⊗ₜ y) = algebraMap R S x * MvPolynomial.aeval P.val y :=
  rfl

variable (P) in
/-- (Implementation detail): The inverse of `tensorModelOfHasCoeffsHom`. -/
noncomputable def tensorModelOfHasCoeffsInv : S →ₐ[R] R ⊗[R₀] P.ModelOfHasCoeffs R₀ :=
  (Ideal.Quotient.liftₐ _
    ((Algebra.TensorProduct.map (.id R R) (Ideal.Quotient.mkₐ _ _)).comp
      (MvPolynomial.algebraTensorAlgEquiv R₀ R).symm.toAlgHom) <| by
    simp_rw [← RingHom.mem_ker, ← SetLike.le_def]
    rw [← P.span_range_relation_eq_ker, Ideal.span_le]
    rintro a ⟨i, rfl⟩
    simp only [AlgEquiv.toAlgHom_eq_coe, SetLike.mem_coe, RingHom.mem_ker, AlgHom.coe_comp,
      AlgHom.coe_coe, Function.comp_apply, algebraTensorAlgEquiv_symm_relation]
    simp only [TensorProduct.map_tmul, AlgHom.coe_id, id_eq, Ideal.Quotient.mkₐ_eq_mk,
      Ideal.Quotient.mk_span_range, tmul_zero]).comp
    (P.quotientEquiv.restrictScalars R).symm.toAlgHom

@[simp]
lemma tensorModelOfHasCoeffsInv_aeval_val (x : MvPolynomial ι R₀) :
    P.tensorModelOfHasCoeffsInv R₀ (MvPolynomial.aeval P.val x) =
      1 ⊗ₜ[R₀] (Ideal.Quotient.mk _ x) := by
  rw [← MvPolynomial.aeval_map_algebraMap R, ← Generators.algebraMap_apply, ← quotientEquiv_mk]
  simp [tensorModelOfHasCoeffsInv, -quotientEquiv_symm, -quotientEquiv_mk]

private lemma hom_comp_inv :
    (P.tensorModelOfHasCoeffsHom R₀).comp (P.tensorModelOfHasCoeffsInv R₀) = AlgHom.id R S := by
  have h : Function.Surjective
      ((P.quotientEquiv.restrictScalars R).toAlgHom.comp (Ideal.Quotient.mkₐ _ _)) :=
    (P.quotientEquiv.restrictScalars R).surjective.comp Ideal.Quotient.mk_surjective
  simp only [← AlgHom.cancel_right h, tensorModelOfHasCoeffsInv, AlgEquiv.toAlgHom_eq_coe,
    AlgHom.id_comp]
  rw [AlgHom.comp_assoc, AlgHom.comp_assoc, ← AlgHom.comp_assoc _ _ (Ideal.Quotient.mkₐ R P.ker),
    AlgEquiv.symm_comp, AlgHom.id_comp]
  ext x
  simp

private lemma inv_comp_hom :
    (P.tensorModelOfHasCoeffsInv R₀).comp (P.tensorModelOfHasCoeffsHom R₀) = AlgHom.id R _ := by
  ext x
  obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
  simp

/-- The natural isomorphism `R ⊗[R₀] S₀ ≃ₐ[R] S`. -/
noncomputable def tensorModelOfHasCoeffsEquiv : R ⊗[R₀] P.ModelOfHasCoeffs R₀ ≃ₐ[R] S :=
  AlgEquiv.ofAlgHom (P.tensorModelOfHasCoeffsHom R₀) (P.tensorModelOfHasCoeffsInv R₀)
    (P.hom_comp_inv R₀) (P.inv_comp_hom R₀)

@[simp]
lemma tensorModelOfHasCoeffsEquiv_tmul (x : R) (y : MvPolynomial ι R₀) :
    P.tensorModelOfHasCoeffsEquiv R₀ (x ⊗ₜ y) = algebraMap R S x * MvPolynomial.aeval P.val y :=
  rfl

@[simp]
lemma tensorModelOfHasCoeffsEquiv_symm_tmul (x : MvPolynomial ι R₀) :
    (P.tensorModelOfHasCoeffsEquiv R₀).symm (MvPolynomial.aeval P.val x) =
      1 ⊗ₜ[R₀] (Ideal.Quotient.mk _ x) :=
  tensorModelOfHasCoeffsInv_aeval_val _ x

end Algebra.Presentation
